\begin{tabbing}
(\=(((ParallelOp ( {-}1)$\cdot$) \+
\\[0ex]CollapseTHEN (((((if (first\_bool T:b
\-\\[0ex])\= then HypSubst' else RevHypSubst') ( {-}1)( 0))$\cdot$) \+
\\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$))$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN (((RWO "append\_assoc" 0) 
\\[0ex]CollapseTHENA (Auto$\cdot$))$\cdot$))$\cdot$
\-
\end{tabbing}